E:Type, dE:EqDecider(E), dL:EqDecider(IdLnk), V:(KndIdType), pred?:(E(E+Unit)),
info:(E(IdId+(IdLnkE)Id)), val:(e:EV(kind(e),loc(e))),
p:(e:E, l:IdLnk.
p:(e':E.
p:(e'':E.
p:(rcv?(e'')
p:( sender(e'') = e
p:( link(e'') = l
p:( e'' = e'  e'' < e' & loc(e') = destination(l)  Id), e:E, l:IdLnk.
SWellFounded(first(y) & x = pred(y)  E)
 sends(dE;dL;pred?;info;val;p;e;l)  Msg(l,tg. V(rcv(l,tg),destination(l))) List 

latex

Definitions	P  Q, SWellFounded(R(x;y)), x,y. t(x;y), A & B, A, first(e), pred(e), x:A. B(x), rcv?(e), sender(e), link(e), P & Q, P  Q, e < e', Prop, Unit, Knd, EqDecider(T), sends(dE;dL;pred?;info;val;p;e;l), receives(dE;dL;pred?;info;p;e;l), rcv-from-on(dE;dL;info;e;l;r), map(f;as), Msg(M), rcv(l,tg), destination(l), rmsg(info;val;e), P  Q, S  T, S  T, kind(e), loc(e), Id, IdLnk, t  T, x:A. B(x), b
Lemmas	loc wf, kind wf, rmsg wf, ldst wf, rcv wf, Msg wf, map wf, rcv-from-on wf, assert wf, Id wf, receives wf, deq wf, IdLnk wf, Knd wf, unit wf, cless wf, link wf, sender wf, rcv? wf, pred wf, first wf, not wf, strongwellfounded wf, assert-rcv-from-on